Java Modeling Language
part 6/8 · 12.1 KB total
──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
Tool support
A variety of tools provide functionality based on JML annotations. The Iowa State JML tools provide an assertion checking compiler jmlc which converts JML annotations into runtime assertions, a documentation generator jmldoc which produces Javadoc documentation augmented with extra information from JML annotations, and a unit test generator jmlunit which generates JUnit test code from JML annotations.
Independent groups are working on tools that make use of JML annotations. These include:
• ESC/Java2 [1], an extended static checker which uses JML annotations to perform more rigorous static checking than is otherwise possible.
• OpenJML declares itself the successor of ESC/Java2.
• Daikon, a dynamic invariant generator.
• KeY, which provides an open source theorem prover with a JML front-end and an Eclipse plug-in (JML Editing) with support for syntax highlighting of JML.
• Krakatoa, a static verification tool based on the Why verification platform and using the Coq proof assistant.
• JMLEclipse, a plugin for the Eclipse integrated development environment with support for JML syntax and interfaces to various tools that make use of JML annotations.
──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────